alle{-}at2(${\it es}$; $i$; $x_{1}$; $x_{2}$; $x_{1}$,$x_{2}$.$P$($x_{1}$;$x_{2}$)) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$alle{-}at(${\it es}$;$i$;$e$.$P$(es{-}when(${\it es}$; $x_{1}$; $e$);es{-}when(${\it es}$; $x_{2}$; $e$)))